Step of Proof: fseg_transitivity 11,40
Inference at * 
Iof proof for Lemma fseg transitivity:


  T:Type, l1, l2, l3:(T List). fseg(T;l1;l2)  fseg(T;l2;l3)  fseg(T;l1;l3) 
latex
 by ((((((((Unfold `fseg` 0) 
CollapseTHEN (Auto'))) 
CollapseTHEN (D (-1)))) 
CollapseTHEN (
CExRepD))) 
CollapseTHEN (((WeakSubstFor l3 0) 
CollapseTHEN (WeakSubstFor l2 0)))) 
latex

C1: 

C1: 1. T : Type
C1: 2. l1 : T List
C1: 3. l2 : T List
C1: 4. l3 : T List
C1: 5. L1 : T List
C1: 6. l2 = (L1 @ l1)
C1: 7. L : T List
C1: 8. l3 = (L @ l2)
C1:   L@0:T List. ((L @ L1 @ l1) = (L@0 @ l1))
C.

Definitionsfseg(T;L1;L2), A List, [], x:A.B(x), Void, i  j , A  B, P  Q, P  Q, P & Q, [car / cdr], SQType(T), P  Q, {T}, s ~ t, , S  T, Top, {x:A| B(x)} , ||as||, x:A. B(x), x:A  B(x), as @ bs, , type List, x:A. B(x), x:AB(x), s = t, t  T, , Type
Lemmasnon neg length, cons one one, guard wf, nat wf, length wf nat, top wf, append wf, member wf

origin